\begin{tabbing}
(\%L:wf\% 
\\[0ex]\% \=if hyp i is not a declaration, then quantifier type \+
\\[0ex]
\\[0ex]will already be on the lhs of the $>>$ \% 
\-\\[0ex]$\backslash$p. 
\\[0ex]if is\_visible\_var (var\_of\_hyp (
\\[0ex]get\_int\_arg `i` p + 2) p) then 
\\[0ex](\=(At (get\_term\_arg `UA` p) (D 0)) \+
\\[0ex]CollapseTHENA (
\-\\[0ex]M\=emCD THENL [SoftNthHyp ({-}3);((BackThruHyp ({-}2)) \+
\\[0ex]CollapseTHEN (NthDecl ({-}1)))$\cdot$]))$\cdot$ p 
\\[0ex]
\-\\[0ex]el\=se \+
\\[0ex]Id p)
\-
\end{tabbing}